Strategic Computation and Deduction
Identifieur interne : 004522 ( Main/Exploration ); précédent : 004521; suivant : 004523Strategic Computation and Deduction
Auteurs : Claude Kirchner [France] ; Florent Kirchner [France] ; Helene Kirchner [France]Source :
English descriptors
- mix :
Abstract
We introduce the notion of abstract strategies for abstract reduction systems. Adequate properties of termination, confluence and normalization under strategy can then be defined. Thanks to this abstract concept, we draw a parallel between strategies for computation and strategies for deduction. We define deduction rules as rewrite rules, a deduction step as a rewriting step and a proof construction step as a narrowing step in an adequate abstract reduction system. Computation, deduction and proof search are thus captured in the uniform foundational concept of abstract reduction system in which abstract strategies have a clear formalisation.
Url:
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Hal, to step Corpus: 004833
- to stream Hal, to step Curation: 004833
- to stream Hal, to step Checkpoint: 003541
- to stream Main, to step Merge: 004647
- to stream Main, to step Curation: 004522
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">Strategic Computation and Deduction</title>
<author><name sortKey="Kirchner, Claude" sort="Kirchner, Claude" uniqKey="Kirchner C" first="Claude" last="Kirchner">Claude Kirchner</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-104751" status="VALID"><idno type="RNSR">200818243Z</idno>
<orgName>INRIA Bordeaux - Sud-Ouest</orgName>
<desc><address><addrLine>200, avenue de la Vieille Tour, 33405 Talence</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/bordeaux/</ref>
</desc>
<listRelation><relation active="#struct-300009" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-300009" type="direct"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName>
<orgName type="acronym">Inria</orgName>
<desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/en/</ref>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>France</country>
</affiliation>
</author>
<author><name sortKey="Kirchner, Florent" sort="Kirchner, Florent" uniqKey="Kirchner F" first="Florent" last="Kirchner">Florent Kirchner</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-2071" status="VALID"><orgName>Laboratoire d'informatique de l'École polytechnique [Palaiseau]</orgName>
<orgName type="acronym">LIX</orgName>
<desc><address><addrLine>Route de Saclay 91128 PALAISEAU CEDEX</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.lix.polytechnique.fr/</ref>
</desc>
<listRelation><relation active="#struct-300340" type="direct"></relation>
<relation name="UMR7161" active="#struct-441569" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-300340" type="direct"><org type="institution" xml:id="struct-300340" status="VALID"><orgName>Polytechnique - X</orgName>
<desc><address><country key="FR"></country>
</address>
</desc>
</org>
</tutelle>
<tutelle name="UMR7161" active="#struct-441569" type="direct"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno>
<idno type="IdRef">02636817X</idno>
<orgName>Centre National de la Recherche Scientifique</orgName>
<orgName type="acronym">CNRS</orgName>
<date type="start">1939-10-19</date>
<desc><address><country key="FR"></country>
</address>
<ref type="url">http://www.cnrs.fr/</ref>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>France</country>
</affiliation>
</author>
<author><name sortKey="Kirchner, Helene" sort="Kirchner, Helene" uniqKey="Kirchner H" first="Helene" last="Kirchner">Helene Kirchner</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-104751" status="VALID"><idno type="RNSR">200818243Z</idno>
<orgName>INRIA Bordeaux - Sud-Ouest</orgName>
<desc><address><addrLine>200, avenue de la Vieille Tour, 33405 Talence</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/bordeaux/</ref>
</desc>
<listRelation><relation active="#struct-300009" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-300009" type="direct"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName>
<orgName type="acronym">Inria</orgName>
<desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/en/</ref>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>France</country>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">HAL</idno>
<idno type="RBID">Hal:inria-00433745</idno>
<idno type="halId">inria-00433745</idno>
<idno type="halUri">https://hal.inria.fr/inria-00433745</idno>
<idno type="url">https://hal.inria.fr/inria-00433745</idno>
<date when="2008">2008</date>
<idno type="wicri:Area/Hal/Corpus">004833</idno>
<idno type="wicri:Area/Hal/Curation">004833</idno>
<idno type="wicri:Area/Hal/Checkpoint">003541</idno>
<idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">003541</idno>
<idno type="wicri:Area/Main/Merge">004647</idno>
<idno type="wicri:Area/Main/Curation">004522</idno>
<idno type="wicri:Area/Main/Exploration">004522</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en">Strategic Computation and Deduction</title>
<author><name sortKey="Kirchner, Claude" sort="Kirchner, Claude" uniqKey="Kirchner C" first="Claude" last="Kirchner">Claude Kirchner</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-104751" status="VALID"><idno type="RNSR">200818243Z</idno>
<orgName>INRIA Bordeaux - Sud-Ouest</orgName>
<desc><address><addrLine>200, avenue de la Vieille Tour, 33405 Talence</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/bordeaux/</ref>
</desc>
<listRelation><relation active="#struct-300009" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-300009" type="direct"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName>
<orgName type="acronym">Inria</orgName>
<desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/en/</ref>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>France</country>
</affiliation>
</author>
<author><name sortKey="Kirchner, Florent" sort="Kirchner, Florent" uniqKey="Kirchner F" first="Florent" last="Kirchner">Florent Kirchner</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-2071" status="VALID"><orgName>Laboratoire d'informatique de l'École polytechnique [Palaiseau]</orgName>
<orgName type="acronym">LIX</orgName>
<desc><address><addrLine>Route de Saclay 91128 PALAISEAU CEDEX</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.lix.polytechnique.fr/</ref>
</desc>
<listRelation><relation active="#struct-300340" type="direct"></relation>
<relation name="UMR7161" active="#struct-441569" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-300340" type="direct"><org type="institution" xml:id="struct-300340" status="VALID"><orgName>Polytechnique - X</orgName>
<desc><address><country key="FR"></country>
</address>
</desc>
</org>
</tutelle>
<tutelle name="UMR7161" active="#struct-441569" type="direct"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno>
<idno type="IdRef">02636817X</idno>
<orgName>Centre National de la Recherche Scientifique</orgName>
<orgName type="acronym">CNRS</orgName>
<date type="start">1939-10-19</date>
<desc><address><country key="FR"></country>
</address>
<ref type="url">http://www.cnrs.fr/</ref>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>France</country>
</affiliation>
</author>
<author><name sortKey="Kirchner, Helene" sort="Kirchner, Helene" uniqKey="Kirchner H" first="Helene" last="Kirchner">Helene Kirchner</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-104751" status="VALID"><idno type="RNSR">200818243Z</idno>
<orgName>INRIA Bordeaux - Sud-Ouest</orgName>
<desc><address><addrLine>200, avenue de la Vieille Tour, 33405 Talence</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/bordeaux/</ref>
</desc>
<listRelation><relation active="#struct-300009" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-300009" type="direct"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName>
<orgName type="acronym">Inria</orgName>
<desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/en/</ref>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>France</country>
</affiliation>
</author>
</analytic>
</biblStruct>
</sourceDesc>
</fileDesc>
<profileDesc><textClass><keywords scheme="mix" xml:lang="en"><term>computation</term>
<term>deduction</term>
<term>logic</term>
<term>strategy</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">We introduce the notion of abstract strategies for abstract reduction systems. Adequate properties of termination, confluence and normalization under strategy can then be defined. Thanks to this abstract concept, we draw a parallel between strategies for computation and strategies for deduction. We define deduction rules as rewrite rules, a deduction step as a rewriting step and a proof construction step as a narrowing step in an adequate abstract reduction system. Computation, deduction and proof search are thus captured in the uniform foundational concept of abstract reduction system in which abstract strategies have a clear formalisation.</div>
</front>
</TEI>
<affiliations><list><country><li>France</li>
</country>
</list>
<tree><country name="France"><noRegion><name sortKey="Kirchner, Claude" sort="Kirchner, Claude" uniqKey="Kirchner C" first="Claude" last="Kirchner">Claude Kirchner</name>
</noRegion>
<name sortKey="Kirchner, Florent" sort="Kirchner, Florent" uniqKey="Kirchner F" first="Florent" last="Kirchner">Florent Kirchner</name>
<name sortKey="Kirchner, Helene" sort="Kirchner, Helene" uniqKey="Kirchner H" first="Helene" last="Kirchner">Helene Kirchner</name>
</country>
</tree>
</affiliations>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 004522 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 004522 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien |wiki= Wicri/Lorraine |area= InforLorV4 |flux= Main |étape= Exploration |type= RBID |clé= Hal:inria-00433745 |texte= Strategic Computation and Deduction }}
This area was generated with Dilib version V0.6.33. |